EOrderAxioms(E; pred?; info)
== (e:E, l:IdLnk.
== (e':E.
== (e'':E.
== (rcv?(e'')  sender(e'') = e  link(e'') = l  e'' = e'  e'' < e' & loc(e') = destination(l))
== & (e, e':E. loc(e) = loc(e')  pred?(e) = pred?(e')  e = e')
== & SWellFounded(pred!(e;e'))
== & (e:E. first(e)  loc(pred(e)) = loc(e))
== & (e:E. rcv?(e)  loc(sender(e)) = source(link(e)))
== & (e, e':E. rcv?(e)  rcv?(e')  link(e) = link(e')  sender(e) < sender(e')  e < e') 

latex

---

clarification:

EOrderAxioms{i}(E;
EOpred?;
EOinfo)
== (e:E, l:IdLnk.
== (e':E.
== (e'':E.
== (rcv?(info;e'')
== ( sender(info;e'') = e  E
== ( link(info;e'') = l  IdLnk
== ( e'' = e'  E  cless(E;pred?;info;e'';e') & loc(info;e') = destination(l)  Id)
== & (e:E, e':E. loc(info;e) = loc(info;e')  Id  pred?(e) = pred?(e')  E+Unit  e = e'  E)
== & strongwellfounded(E; e,e'.pred!(E;pred?;info;e;e'))
== & (e:E. first(pred?;e)  loc(info;pred(pred?;e)) = loc(info;e)  Id)
== & (e:E. rcv?(info;e)  loc(info;sender(info;e)) = source(link(info;e))  Id)
== & (e:E, e':E.
== & (rcv?(info;e)
== & ( rcv?(info;e')
== & ( link(info;e) = link(info;e')  IdLnk
== & ( cless(E;pred?;info;sender(info;e);sender(info;e'))
== & ( cless(E;pred?;info;e;e')) 

latex

Definitions	x:A. B(x), P  Q, destination(l), left+right, Unit, f(a), SWellFounded(R(x;y)), pred!(e;e'), A, first(e), pred(e), P & Q, Id, loc(e), source(l), x:A. B(x), b, rcv?(e), s = t, IdLnk, link(e), P  Q, sender(e), e < e'
FDL editor aliases	EOrderAxioms